Notes (Week 10 Thursday)

Q1

D)

i)
Frame

--------------
(Not []) Frame

      e Expr
----------------
(And [] e) Frame

     v Value
----------------
(And v []) Frame


ii)
Stack

These will generally be of the form: _ |> _ |> _ o

Empty stack case:

-------
o Stack

Non-empty stack case:

f Frame   s Stack
-----------------
  f |> s Stack


iii)

Initial:
o > e

Final:
o < v


iv)

Not an axiom, because it has conditions above the line:

v is a member of {True, False}
------------------------------
      s > v |-> s < v

Axioms:

---------------------
s > True |-> s < True

-----------------------
s > False |-> s < False

(Note: s can include the entire stack terminated by a `o`)

-----------------------------------
s > (Not e)  |->  (Not []) |> s > e

------------------------------------
(Not []) |> s < True  |->  s < False

------------------------------------
(Not []) |> s < False  |->  s < True

-------------------------------------------
s > (And e1 e2)  |->  (And [] e2) |> s > e1

------------------------------------
(And [] e2) |> s < True  |->  s > e2

----------------------------------------
(And [] e2) |> s < False  |->  s < False


let x = 3 in
    (let x = 5
        in x + 1) + x


Q2

A)

i) Function closure:

   (NB: Closures can be a computation with the
   environment `eta` in which it should be executed.
      <<eta, x + x>>
   where eta  might contain x = 7)

   A value representing the function, the names it binds
   for itself and its argument, and the expression that
   defines it (resp. f, x, e), as well as the environment
   `eta` in which it should be executed,
   of form <<eta, f. x. e>>.

ii)
   s is a stack
   eta is an environment

   s | eta > (Recfun (f. x. x + 1))

   this would result in closure

   <<eta, f. x. x + 1>>


Q3

B) manual type inference

i) forall a b. a + (Bool + b)


C) g is of universal type
     - takes a pair of values both of *any* arbitrary type `a`,
       and returns a value of that type
     - used for parametrically polymorphic functions

   f is of existential type
     - takes a pair of values both of *a fixed but unknown* type
       `a`, and returns a value of that type
     - used for modules

g : forall a. (a, a) -> a

  We are looking for v s.t. g(v) is type correct

  v : (Int, Int)
  v : (Bool, Bool)
  v : (a, a)  where both types are the same

  Answer: v := (2, 3) results in g(v) : Int,
  which is type correct.


f : exists a. (a, a) -> a

  Answer: There is no concrete w s.t. f(w) is type correct,
  because we cannot provide a value of type `(a, a)` where
  `a` is a particular arbitrary type that is unknown to us.
  (Unless you count w = Error, which has any type.)